package geneticsatsolver;

import java.io.BufferedReader;
import java.io.DataInputStream;
import java.io.FileInputStream;
import java.io.InputStreamReader;
import java.util.Iterator;
import java.util.Scanner;
import java.util.Vector;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

/**
 * Class Problem to represent the problem in memeory
 * 
 * @author igor
 */
public class Problem {

    private int curclause = 0;
    private int clausenum = -1;
    private Clause[] problem = null;
    public int n_var = 0;
    public boolean done;

    /**
     * Load problem to memory from file
     *
     * @param filename SAT problem file in CFN format
     */
    public Problem(String filename) {
        try {
            FileInputStream fstream = new FileInputStream(filename);
            DataInputStream in = new DataInputStream(fstream);
            BufferedReader br = new BufferedReader(new InputStreamReader(in));
            String strLine;
            Vector<Integer> clause = new Vector<Integer>();
            while ((strLine = br.readLine()) != null) {
                if (strLine.startsWith("c")) {
                    //ignore comment 
                } else if (strLine.startsWith("p")) {
                    String patternStr = "\\D+(\\d*)\\D+(\\d*)";
                    Pattern pattern = Pattern.compile(patternStr);
                    Matcher matcher = pattern.matcher(strLine);
                    if (matcher.find()) {
                        n_var = Integer.parseInt(matcher.group(1));
                        clausenum = Integer.parseInt(matcher.group(2));
                        problem = new Clause[clausenum];
                    }
                } else {
                    Scanner sc = new Scanner(strLine);
                    while (sc.hasNextInt()) {
                        int literal = sc.nextInt();
                        if (literal != 0) {
                            clause.add(literal);
                        } else if (clause.size() > 0) {
                            this.addClausule((Vector<Integer>) clause.clone());
                            clause.clear();
                        }
                    }
                }
            }
            in.close();
            if (curclause == clausenum) {
                done = true;
            } else {
                done = false;
            }
        } catch (Exception e) {//Catch exception if any
            done = false;
        }
    }

    /**
     * Class Clause to represent a single clause of the problem
     *
     */
    private class Clause {

        private Vector<Integer> literals = new Vector<Integer>();

        /**
         * Initialize clause
         *
         * @param row literals vector in the clause
         */
        private Clause(Vector<Integer> row) {
            literals = row;
        }

        /**
         * Verifiy a clause for a specified assignment
         *
         * @param assignment assignmente to test
         * @return      verify result
         */
        public boolean verify(boolean[] assignment) {
            boolean verified = false;
            Iterator nums = literals.iterator();
            while (nums.hasNext() && !verified) {
                Integer literal = (Integer) nums.next();
                if (literal > 0) {
                    verified = assignment[literal - 1];
                } else {
                    verified = !assignment[-1 * literal - 1];
                }
            }
            return verified;
        }
    }

    /**
     * Add clause to the problem
     *
     * @param row disjunction of literlas to add
     */
    public void addClausule(Vector<Integer> row) {
        problem[curclause++] = new Clause(row);
    }

    /**
     * Verify all clause of the problem for a specified assignment
     * of literals
     *
     * @param assignment assignment to test
     * @return      verify result
     */
    public int verify(boolean[] assignment) {
        int howmanytrue = 0;
        for (int i = 0; i < clausenum; i++) {
            if (problem[i].verify(assignment)) {
                howmanytrue++;
            }
        }
        return howmanytrue;
    }

    /**
     * Get number of clauses in the problem
     *
     * @return      number of clauses
     */
    public int getNumClauses() {
        return clausenum;
    }
}
